FDL - Step of Proof: and_functionality_wrt

Step of Proof: and_functionality_wrt_implies

12,41

Inference at *
Iof proof for Lemma and functionality wrt implies:

P1, P2, Q1, Q2:

. {P1

P2}

{Q1

Q2}

{(P1 & Q1)

(P2 & Q2)}

by ((((Unfold `guard` 0)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (HypBackchain))

Definitions t T, P & Q, {T}, P Q, , x:A. B(x)